Make patch 0005 near upstream speed with in-line F16 checks (#174) - #182

Makes patch 0005 (ggml_vec_dot_f16, #174, upstream ggml-org/llama.cpp#31734) about as fast as unpatched upstream while keeping its overflow guarantee. The first 0005 ran every dot in F32 and cost up to 2x in F16 decode on linux_armv8.2_2.

Design

Same approach as 0006 (#179), for non-SVE NEON with FP16 vector arithmetic. x86, SVE and MSVC paths are unchanged.

• Rows of up to 2048 elements (64 products per lane) run upstream's F16 multiply-adds and F16 reduction in its order, in-line. A NaN check on the reduced F16 vector (sum - sum == 0 in every lane) runs before conversion to F32. The double scalar tail is upstream's.
• Longer rows run out of line (noinline): each 64-step block is reduced the same way and added into F32 lanes, with an isfinite check on the F32 sum before the tail.
• A nonfinite row is computed again by the first 0005 (noinline, FMLAL/FMLAL2 with FP16 FML, otherwise conversion plus F32 FMA). A cold attribute made an all-overflow matrix 4.3x slower, so the recompute is only noinline plus __builtin_expect.

Contract

• Finite F16 inputs never give a nonfinite result. An overflowed row, or one with a NaN or inf input before the scalar tail, matches the first 0005 bit for bit. NaN and inf inputs still propagate (as upstream in the tail).
• For n < 2080 (one block plus tail), every finite result is bit-identical to unpatched upstream. Longer rows add their per-block F16 sums in F32. Within a block, F16 rounding is upstream's, so results are not F32-accurate.
• Cost: one F16-vector check per row. A recomputed row runs both the F16 and the F32 pass.

Tests and mutants

tests/f16_dot_accumulation_test.cpp now models the patched dot exactly: upstream's F16 multiply-adds per lane, its reduction order, 64-step blocks, F32 lanes and the double tail. It needs a bit-exact match wherever the model is finite. New cases:

• block-boundary exactness and F16 rounding;
• lane and split-sign overflows in one-block and multi-block rows;
• maximum tails, including rows without NaN padding;
• NaN and inf inputs.

Mutants were run on the Apple FMLAL build and the conversion build (GGML_CPU_ARM_ARCH=armv8.2-a+fp16+dotprod), with identical results:

29 of the 30 mutants are killed. The one survivor is equivalent.

Performance

Qwen2.5-0.5B-Instruct (F16 and Q8_0), CPU, 8 threads, F16 KV. Each value is new 0005 + 0006 relative to unpatched v0.9.0, as the median over interleaved rounds (5 on M4, 3 on GCE). Ranges cover FA off/on and both decode tests.

• Compared with 0006 alone, new 0005 measures 0.97–1.02 on decode rows. The lowest, 0.97, is t2a F16 tg128 FA off, and the same row's round-to-round spread is ±0.015. Prefill measures 0.98–1.00 on every host except linux_armv8.6_1, where F16 is 0.98 / 0.99 and Q8_0 FA off is 0.98. On that variant llamafile is compiled out under I8MM, so every F16 matmul goes through ggml_vec_dot_f16 and the per-row check is visible. The remaining M4 F16 prefill gap is 0006: 0006 alone measures 0.93 / 0.94.
• Kernel on M4, one thread, against the unpatched kernel, for rows of 64 / 128 / 256 / 4096 elements:
  • FMLAL build: +4% / +12% / +2% / −3%
  • conversion build: +2% / +5% / +1% / −3%
  • first 0005 at 4096: +14% (FMLAL) / +78% (conversion)
  • all rows overflowing: 2.1x (FMLAL) / 2.75x (conversion)
• No benchmark produced a nonfinite logit.

Verification

• Follow-ups from CI:
  • tools/linux_cpu_variant_smoke.c now allows the error of four F16 roundings (2^-9 × absolute sum) on its 64-element dot. The first 0005 was F32-accurate, so the old 2e-6 bound broke at magnitude 30 (83328 against 83313). The failure reproduced on M4 and passes there with the new bound.
  • NaN/inf input cases now run only on the patched path. In debug builds, upstream's other F16 dot paths assert a finite sum. An armv8-a Debug build on M4 reproduced the x86 abort, and passes with the fix.
• F16 test: PASS on the Apple FMLAL, conversion, no-llamafile and ASan builds, and on linux_armv8.2_2/linux_armv8.6_1/baseline modules on Neoverse-N1 and Neoverse-V2. GCE built the hot path with cold on the recompute; that hot path is instruction-identical to this head.
• tools/llama_cpp_patches.py apply --strict: 0005 alone applies on v0.7.0, v0.8.0 and v0.9.0; the full series applies on v0.8.0 and v0.9.0.
• tools/validate_linux_arm64_cpu_isa.py passes on both Linux modules, which are GCC 13.3 builds of this head. In linux_armv8.6_1, FMLAL appears only in the recompute (10 instructions) and in 0006. linux_armv8.2_2 has no FMLAL.
• Python suite: 449 tests OK, 1 skipped.

High-risk native kernel change. Independent audit: ACCEPT at 57a8aa43 against main eb760895, with no blocking findings.

• Analysis: finite inputs cannot escape the check, and dispatch is unchanged outside the patched path.
• Fuzz: bit-exact against scalar emulations of upstream and of the old 0005. About 1.44M calls, plus 240k per module on Neoverse N1 and V2, gave 0 mismatches, 0 contract failures and 0 over-reads.
• GCE re-measured at the exact head: every host is at 0.97× or better against unpatched v0.9.0. F16 prefill on armv8.2_2 is 1.47–1.49×.
• Follow-up (test-only): add a negative-only overflow case (two contract-breaking mutants survive the test but are caught by the fuzz), pin the bit-identity of recomputed rows and the F32 lane order, and restore the 2e-6 smoke tolerance for the F32 control case.